#load "spitree.cmo";;
#load "spiparser.cmo";;
#load "spilexer.cmo";;
#load "aconv.cmo";;
#load "auxilirary.cmo";;

open Spitree
open Auxilirary
open Unix;;

(* Judgment of well-formedness of an environment
 * Input: list env_element env - Environment to judge
 * Output: bool, indicating well-formedness
 *)
exception EnvFailure of string;;
let rec env_judgment env =
  match env with
    | [] -> true
    | Type(x, t)::env_rest ->
(*	Printf.printf "Environment: [%s]\n" (string_of_env env);
	Printf.printf "Fn of %s in domain of [%s]: %B\n" (string_of_typ t) (string_of_env env_rest) (SSet.subset (fn_typ t) (dom env_rest));
	Printf.printf "Name %s not in domain of [%s]: %B\n" x (string_of_env env_rest) (not (SSet.mem x (dom env_rest)));*)
	(*Printf.printf "%B\n" (env_judgment env_rest);*)
	let good =
	  ((SSet.subset (fn_typ t) (dom env_rest)) &
	  (not (SSet.mem x (dom env_rest))) &
          (env_judgment env_rest)) in
	if good then true else
	  raise (EnvFailure ("Type declaration " ^ (string_of_env_element (Type(x, t))) ^ " inconsistent with environment " ^ (string_of_env env_rest)))
    | Effect(r)::env_rest ->
	let good =
	  ((SSet.subset (fn_res r) (dom env_rest)) &
	  env_judgment env_rest) in
	if good then true else
	  raise (EnvFailure ("Effect " ^ (string_of_env_element (Effect(r))) ^ "inconsistent with environment " ^ (string_of_env env_rest)));;

(* Judgment of the goodness of a message
 * Input:
 * list env_element env - Environment
 * msg msg - Message
 * typ typ - Type
 * Output: bool, indicating if msg is good with type typ in environment env
 *)
exception MsgTypeFailure of string;;
let rec msg_judgment env msg typ =
  let pair_judgment env m t n u =
    (msg_judgment env m t) &
    (msg_judgment env n u) in
  let encrypt_judgment env m t n ntype =
    (msg_judgment env m t) &
    (msg_judgment env n ntype) in
  match msg with
    | MPair(m, n) ->
	(match typ with
	  | TPair(x, t, u) ->
	      pair_judgment env m t n (subst_name u x m)
	  | Un ->
	      pair_judgment env m Un n Un
	  | _ -> raise (MsgTypeFailure ("Message " ^ (string_of_msg msg) ^ " can not have type " ^ (string_of_typ typ))))
    | Encr(m, Name(x)) ->
	(if (typ = Un) then
	   let n, keytype = (Name(x), (nametype x env)) in
	   (match keytype with
	      | Key(t) ->
		  encrypt_judgment env m t n keytype
	      | Un ->
		  encrypt_judgment env m Un n Un
	      | _ -> raise (MsgTypeFailure ("Key " ^ (string_of_msg n) ^ " can not have type " ^ (string_of_typ keytype))))
	 else
	   raise (MsgTypeFailure ("Encrypted message " ^ (string_of_msg msg) ^ " must have type Un, but is given type " ^ (string_of_typ typ))))
    | Encr(m, n) ->
	(if (typ = Un) then
	   encrypt_judgment env m Un n Un
	 else
	   raise (MsgTypeFailure ("Encrypted message " ^ (string_of_msg msg) ^ " must have type Un, but is given type " ^ (string_of_typ typ))))
    | Name(x) ->
	(*Printf.printf "Name judgment: %s\n" x;*)
	let ntype = nametype x env in
	let good =
	  ((type_equal 0 ntype typ) &
	     (SSet.mem x (dom env)) &
	     (env_judgment env)) in
	  if good then
	    true
	  else
	    raise (MsgTypeFailure ("Type of name " ^ x ^ " inconsistent"))
    | Ok ->
	(*Printf.printf "Ok judgment\n";*)
	(match typ with
	   | Un ->
	       env_judgment env
	   | TOk(s) ->
(*	       Printf.printf "Effects of %s in\n" (string_of_reso s);
	       Printf.printf "%s\n" (string_of_env env);*)
	       (effectinclusion (effect_to_list s) (effects env)) &
		 (SSet.subset (fn_typ typ) (dom env)) &
		 (env_judgment env)
	   | _ -> raise (MsgTypeFailure "ok token must have type Un or Ok(S)"))
;;

(* Judgment of the goodness of a process
 * Input:
 * list env_element env - Environment
 * proc proc - Process
 * Output: bool, indicating if process proc is good in environment env
 *)
exception ProcTypeFailure of string;;
let rec proc_judgment env proc =
  let out_judgment env m mtype n t =
    (msg_judgment env m mtype) &
      (msg_judgment env n t) in
  let in_judgment env m mtype x t p =
    (msg_judgment env m mtype) &
      (proc_judgment (Type(x, t)::env) p) in
  let decrypt_judgment env m n ntype y t p =
    (msg_judgment env m Un) &
      (msg_judgment env n ntype) &
      (proc_judgment (Type(y, t)::env) p) in
  let split_judgment env m mtype x t y u p =
    (msg_judgment env m mtype) &
      (proc_judgment (Type(y, u)::Type(x, t)::env) p) in
  let match_judgment env m mtype n t y substu p =
    (msg_judgment env m mtype) &
      (msg_judgment env n t) &
      (proc_judgment (Type(y, substu)::env) p) in
  match proc with
    | Out(Name(x), n) ->
	let m, chantype = (Name(x), (nametype x env)) in
	(match chantype with
	   | Ch(t) ->
	       out_judgment env m chantype n t
	   | Un ->
	       out_judgment env m Un n Un
	   | _ -> raise (ProcTypeFailure ("Channel " ^ (string_of_msg m) ^ "can not have type" ^ (string_of_typ chantype))))
    | Out(m, n) ->
	out_judgment env m Un n Un
    | (In(Name(y), x, p) | InRepl(Name(y), x, p)) ->
	let m, chantype = (Name(y), (nametype y env)) in
	(match chantype with
	   | Ch(t) ->
	       in_judgment env m chantype x t p
	   | Un ->
	       in_judgment env m Un x Un p
	   | _ -> raise (ProcTypeFailure ("Channel " ^ (string_of_msg m) ^ "can not have type" ^ (string_of_typ chantype))))
    | (In(m, x, p) | InRepl(m, x, p)) ->
	in_judgment env m Un x Un p
    | Nu(x, t, p) ->
	(generative t) &
	(proc_judgment (Type(x, t)::env) p)
    | PPara(p, q) ->
	(proc_judgment (List.append (env_of q) env) p) &
	(proc_judgment (List.append (env_of p) env) q)
    | PNil -> true
    | Begin(l, m) ->
	(SSet.subset (fn_msg m) (dom env)) &
	(env_judgment env)
    | End(l, m) ->
	(SSet.subset (fn_msg m) (dom env)) &
	(effectinclusion [Reso(l, m)] (effects env)) &
	(env_judgment env)
    | Decrypt(m, y, t, Name(x), p) ->
	let n, keytype = (Name(x), (nametype x env)) in
	(match keytype with
	   | Key(_) ->
	       decrypt_judgment env m n keytype y t p
	   | Un ->
	       decrypt_judgment env m n Un y Un p
	   | _ -> raise (ProcTypeFailure ("Key " ^ (string_of_msg n) ^ "can not have type" ^ (string_of_typ keytype))))
    | Decrypt(m, y, t, n, p) ->
	decrypt_judgment env m n Un y Un p
    | Split(Name(z), x, t, y, u, p) ->
	let m, pairtype = (Name(z), (nametype z env)) in
	  (match pairtype with
	     | TPair(_, _, _) ->
		 split_judgment env m pairtype x t y u p
	     | Un ->
		 split_judgment env m Un x Un y Un p
	     | _ -> raise (ProcTypeFailure ("Pair " ^ (string_of_msg m) ^ "can not have type " ^ (string_of_typ pairtype))))
    | Split(MPair(m1, m2), x, t, y, u, p) ->
	let m, pairtype = (MPair(m1, m2), TPair(x, t, u)) in
	split_judgment env m pairtype x t y u p
    | Split(m, x, t, y, u, p) ->
	split_judgment env m Un x Un y Un p
    | Match(m, mtype, n, y, usub, p) ->
	(match mtype with
	   | Un ->
	       match_judgment env m Un n Un y Un p
	   | TPair(x, t, u) ->
	       (match_judgment env m mtype n t y usub p) &
		 (type_equal 0 (subst_name u x n) usub)
	   | _ ->
	       raise (ProcTypeFailure ("Message " ^ (string_of_msg m) ^ " can not have type " ^ (string_of_typ mtype))))
;;



(*effects_in_type (TPair("tnavn", Key(TOk(RPair(Reso("send", Name("a")),Reso("send2", Name("b"))))), TOk(Reso("labl", Name("Moha")))));;

dom [Type("muaah", Un); Type("hehe", TOk(RPair(Reso("heigen",Name("Hmm")),Reso("Gnof", Name("Hnah"))))); Effect(Reso("he", Name("hmm")))];;

msg_judgment [Effect(Reso("send", Name("a"))); Type("noegle", (Key(TOk(Reso("send", Name("a")))))); Type("a", Un)] (Encr(Ok, Name("noegle"))) Un;;
*)

(*let infile = "test.spi";;
let instring = "split pair(hej1,hej2) as (hov:T, he:T); nil"
let msgstring = "({ok}noegle, enlabel({ok}noegle))";;
let procstring = "(nil|(nil|(nil|nil)))";;*)

let infile = Sys.argv.(1);;

(*let infile = "signdecrypt.spi";;*)
let filechan = open_in infile

let lexbuf = Lexing.from_channel filechan;;
let ast = Spiparser.process Spilexer.spi_tokens lexbuf;;

let (ast_substituted, accum, substMap) = Aconv.proc_subst ast 0 Aconv.SMap.empty;;

let freevars =
  Aconv.SMap.fold (fun _ name list ->
		      Type(name, Un) :: list) substMap [];;

print_endline "Alpha converted process:";;
print_endline ((string_of_proc ast_substituted) ^ "\n");;

(* We check for robust safety by initializing all
   free variables to be of type Un *)

print_endline "Free names:";;
Aconv.SMap.iter (Printf.printf "%s: %s\n") substMap;;

let judgment = proc_judgment freevars ast_substituted;;
if judgment then
  Printf.printf "Congratulations! This process is robustly safe.\n";
